Update Crux-llvm testing #618
Conversation
Some test inputs do not pass for Yices; expected files for these are omitted in this commit so that those inputs are not tested. After this PR is merged, issues can be created for those non-passing Yices situations with corresponding expected files provided in those issues.
|
Overall, I like the idea here. However, the test suite just fails hard if any one of the solvers isn't installed, and doesn't run any of the other tests. For local development purposes, it would be much nicer if we could just skip or at least gracefully fail tests for solvers that aren't installed. |
|
Good catch! I was so focused on making it work with all the solvers I forgot about working without all the solvers. I've updated it now so that a missing solver doesn't cause the testing to completely abort, however, individual tests for that solver will still fail. For development purposes one could bypass these with a An alternative would be to simply not run tests for which a solver wasn't present. I'm a little undecided on this point, but my general thought is that by defaulting to run tests for all the solvers this will help ensure we don't forget about testing against some of them. As a developer, you can always just create a PR and let the CI system test the other solvers, but this defaults to being thorough unless you use a specific narrowing as described above. Let me know what you think about this, @robdockins and @travitch . |
|
I'm also not sure what the best policy is. My first thought was that as a user I'd probably just want it to run the tests that I have solvers for, otherwise I'll be drowned in failures that I have to manually triage (and then CI will yell at me if I actually messed something up). In that case, we'd want to be careful and maybe have a flag that really forces all solvers to be tested (and turn a failure to find a solver into an overall CI failure) that we could enable for CI. It would be unfortunate if a CI misconfiguration in the future accidentally got through just because no solvers ran. |
|
I think the most convenient would be more or less what @travitch suggests: for local development run tests for all the solvers that are installed, but have some way to force all the solvers to be exercised for CI. |
| @@ -0,0 +1,36 @@ | |||
| [Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction | |||
There was a problem hiding this comment.
Is this supposed to be part of the file, given it has paths from your env in it?
There was a problem hiding this comment.
Yup, I'm working on that right now. The input is a relative path, but somewhere it's getting the fully-rooted path, which isn't good for several reasons. Thanks for catching this!
|
With the merge of the loopmerge functionality and corresponding test changes, this PR has gotten too messy. I will create a sequence of PR's to make incremental steps towards the final goal, starting with #631 |
Switch to using tasty-sugar for better parameterizing tests.
Add yices tests.
Add timeouts to crucible invocations.
Verify stdout/stderr of each crucible invocation independently of the explicit output.